$\forall$$T$, $V$:Type, $A$:($T$$\rightarrow\mathbb{P}$), ${\it dcd\_A}$:($t$:$T$$\rightarrow$Dec($A$($t$))), $f$:(\{$t$:$T$$\mid$ $A$($t$)\} $\rightarrow$$V$), $g$:(\{$t$:$T$$\mid$ $\neg$($A$($t$))\} $\rightarrow$$V$).
\\[0ex][$A$? $f$ : $g$] $\in$ $T$$\rightarrow$$V$